(declare-sort S0 0)

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v8 Bool)
(declare-const r0 Real)
(declare-const r2 Real)
(declare-const r5 Real)
(declare-const v10 Bool)
(push)
(assert (and v2 v0 v5 (> (tanh r2) r0 (tanh r2)) v10))
(check-sat)
(declare-const v12 Bool)
(assert (xor (and (or v1 v2 v5) (<= 0.05 0.5685) v2 v2 (> (tanh r2) r0 (tanh r2))) v1 v12 v10 (= (or v1 v2 v5) v8 v5 v0) (<= 761905677.0 r5) (and (or v1 v2 v5) (<= 0.05 0.5685) v2 v2 (> (tanh r2) r0 (tanh r2))) v0))
(pop)
(declare-const v13 Bool)
(assert (xor v3 v13 (> (tanh r2) r0 (tanh r2)) (> (tanh r2) r0 (tanh r2)) (> (tanh r2) r0 (tanh r2)) (> (tanh r2) r0 (tanh r2)) v2))
(check-sat)
